es:event_system{i:l}, i:Id, k:Knd, L:(Id List). aframe-p(es; i; k; L)  prop{i:l} 

latex

Definitions	False, A  B, x:A. B(x), A c B, x. t(x), (x  l), A, P  Q, P  Q, aframe-p(es; i; k; L), prop{i:l}, t  T, Knd, x:A. B(x), , es_vartype(es; i; x), es_state(es; i), guard(T), sq_type(T), x(s), es-vartype(es; i; x)
Lemmas	event system wf, IdLnk wf, false wf, l member wf, select wf, length wf1, nat wf, es state when wf, es state wf, es state after wf, Id sq, not wf, es-loc wf, Id wf, alle-at wf